\section{Example: A consistent bank account}
We elaborate here on a simple scenario showing how the type systems can help the design of  consistent systems. 

Our scenario consists of three actors: a bank, a user and an updater. 
The bank consist basically of an account and a service that can be accessed by users for retrieving money. In our example, the user can open a session with the retrieving service of the bank, during the sessions he communicates the amount he needs and awaits confirmation. Dually, the retrieving service awaits for the communication of the amount needed and then opens a session with the account. During this session, it communicates the amount of money and awaits confirmation. Then it closes the sessions with the account and communicates the results to the client.
The updater represents an external entity that can update the services provided by the bank: i.e.,  to add new functionalities, to correct errors, etc. 


We model our system as a parallel composition of the following processes: $Acc \parallel Retr \parallel Client \parallel Upd$ where the actors are defined as follows:

$$
\begin{array}{ll}
Retr &::= \component{r}{0}{\Delta}{\rec{X:\type{\emptyset}{\Delta}}{X \parallel \open{c:\rho_1}. c(x). \\
  & \qquad \ \open{a:\rho_2}.\outC{a}{x}.a(y).\close{a}.\outC{c}{y}.\close{c} } }\\
Acc  &::= \rec{X:\type{\emptyset}{\Delta}}{X \parallel \\
& \qquad \ \open{a:\overline{\rho_2}}.a(x).\outC{a}{ok}.\close{a}}\\
Client&::= \open{c:\overline{\rho_1}}. \outC{c}{m}. c(y).\close{c}

\end{array}
$$

The process $Upd$ is used to update bank services, here we show some possible pattern templates that can 1. completely replace the service, 2. add new functionalities, keeping the existing ones, or 3. make copies of the existing services for instance for backup purposes.

\begin{enumerate}[(1)]
\item Replacement: $ Upd ::= \updated{r}{X}{\Delta}{\Delta'}{\component{r}{0}{\Delta'}{P}}$ where $\mathsf{X} \not \in P$ and $\Delta'$ is the interface of $P$. As $\mathsf{X}$ does not appear in $P$ the whole content of the adaptable process $r$ is thrown away and replaced with a new process $P$.

\item Plug-in: $\updated{r}{X}{\Delta}{\Delta_1}{\component{r}{0}{\Delta'}{\mathsf{X} \parallel P}}$. The update will then result in preserving the old behavior of the retrieving service, to this we add in parallel some additional operations given by $P$.

\item Backup: $\updated{r}{X}{\Delta}{\Delta}{\component{r}{0}{\Delta}{\mathsf{X}} \parallel \component{b}{0}{\Delta}{\mathsf{X}}}$. Here the aim is to duplicate the content of the adaptable process $r$: we recreate the adaptable process and we add a new copy that can act as a backup copy.
\end{enumerate}


In this scenario, the type systems helps in ensuring that no session, and in particular no open session between a client and the retrieving service will be interrupted by an update. Thus all updates are "suspended" until all clients have finished interacting with the bank.


%\section{Example: Context-aware Services}\label{sec:example}
%The proliferation of different means to access services on the Web (e.g., tablets and smart phones) and the amount of information that these devices can collect from the environment (typically people locations) have raised the problem of building services that can adapt to the  context. Here we show how our session-typed framework can support the modeling of context-aware web services. 
%
%The two main features of our proposal are indeed essential to model these systems. First, adaptable processes can easily represent the different components in a web service scenario: servers, services inside servers, and clients. Then, our construct for process update gives us a powerful tool to implement several operations: (i) updates of the whole service---for instance, to  handle an error or to add a new functionality and (ii) updates to adapt the web service to meet the client requirements. Finally, the type system ensures that communications and evolvability steps coexist in a safe way.
%
%As an example, we consider the interaction between a client and a server as the process $Server \parallel Client$. 
%$Server$ is defined by an adaptable process $S$ that contains a travel agency service located at $t$ (not specified here) and a recursive process that handles communications with the clients. We can imagine that the process in $t$ is the core engine of the travel agency. 
%This engine is then updated depending on the context information communicated by the client. 
%Thus, when a communication is established, the first thing that the client sends is the information about the context. 
%In this example, we just consider that the client is sending information on the type of device she is using to contact the server: a laptop (1), a tablet (2) or a smart phone (3). This information is used to select the most suitable update for $t$.
%More precisely, $Server$ is defined as:
%\begin{multline*}
%\component{S}{0}{\Delta}{\component{t}{0}{\Delta_1}{A} \parallel \rec{X:\type{\emptyset}{\rho}}{X \parallel \\
%\open{d:\rho}. \branch{d}{1: P_1; 2:P_2 ; 3:P_3}} }
%\end{multline*}
%where $P_i := \close{d}.\updated{t}{X}{\Delta_1}{\Delta_2}{\component{t}{0}{\Delta_1}{\mathsf{X}} \parallel U_i}$, 
%and $U_i$ is the process that adapts to the specific context.
% $\Delta, \Delta_1$ and $\Delta_2$ depend on the specific implementation, and $\rho = d:\&\{1:\epsilon \vee 2:\epsilon \vee 3: \epsilon\}.\epsilon$.
%In turn, supposing that the $Client$ is working on a tablet: 
%$$
%\component{C}{0}{\Delta'}{\open{d:\overline{\rho}}.\select{2}.\close{d}.P}
%$$
%where $P$ is the process handling the communication with the travel agency.
%Under the empty environment we have: $$\judgement{\emptyset}{\emptyset}{Server \parallel Client}{\emptyset}{\{\overline{\rho}\} \shortmid \{\rho\} \uplus \Delta \uplus \Delta'}$$
%
%To illustrate a typing derivation, we suppose that  we have
%$$Server \parallel Client \pired \restr{d}{Server' \parallel Client'}$$ 
%via rule \rulename{r:Open}, where 
%\begin{eqnarray*}
%Client' & \equiv & \component{C}{1}{\Delta' \ominus \overline{\rho}}{\select{2}.\close{d}.P} \\
%Server' & \equiv & \component{S}{1}{\Delta \ominus \rho}{\component{t}{0}{\Delta_1}{A} \parallel \branch{d}{1: P_1; 2:P_2 ; 3:P_3} \parallel \\
%& & \qquad \quad \rec{X:\type{\emptyset}{\rho}}{X \parallel \\
%& & \qquad \quad  \open{d:\rho}. \branch{d}{1: P_1; 2:P_2 ; 3:P_3}}   }
%\end{eqnarray*}
%For the sake of space, we only type process $Client'$ in Table~\ref{tab:example}.
%
%\begin{table*}
%$$
%\rightinfer[\rulename{Loc}]{\judgement{\emptyset}{\emptyset}{\component{C}{1}{\Delta' \ominus \overline{\rho}}{\select{2}.\close{d}.P}}{\oplus\{1:\rho_1 \vee 2:\epsilon \vee 3:\rho_3 \}}{\Delta' \ominus \overline{\rho}}}
%{\rightinfer[\rulename{Select}]{\judgement{\emptyset}{\emptyset}{\select{2}.\close{d}.P}{\oplus\{1:\rho_1 \vee 2:\epsilon \vee 3:\rho_3 \}}{\Delta' \ominus \overline{\rho}}}{\rightinfer{\judgement{\emptyset}{\emptyset}{P}{\emptyset}{\Delta' \ominus \overline{\rho}}}{}} & 1=1}
%$$
%\caption{Example of typing} \label{tab:example}
%\end{table*}
%
%Observe how the annotation on the active sessions on adaptable process $S$ is what forbids every update action
%on the Server while the session with the client is active.